%==============================================================================
% Enunciado
%==============================================================================

% Formalizar en OTTER la siguiente argumentación y comprobar su validez:
% "Alberto y Juan trabajan juntos. Juan trabaja con todos los comerciales. La
% gripe se contagia irremediablemente en el trabajo. Hay un comercial
% contagiado de gripe. Por tanto, alberto tiene la gripe."

%==============================================================================
% Formalización
%==============================================================================

set(auto2).

formula_list(sos).

% Alberto y Juan trabajan juntos.
  trabaja(Alberto,Juan).

% Juan trabaja con todos los comerciales.
  all x (comercial(x) -> trabaja(Juan,x)).

% La gripe se contagia irremediablemente en el trabajo.
  all x y (gripe(x) & trabaja(x,y) -> gripe(y)).

% La relación 'trabaja' es simétrica.
  all x y (trabaja(x,y) -> trabaja(y,x)).

% Hay un comercial contagiado de gripe.
  exists x (comercial(x) & gripe(x)).

% Conclusión: Alberto tiene la gripe.
  - gripe(Alberto).

end_of_list.

%==============================================================================
